00100		Remarks on the Human Engineering of the new Proof Checker
00200	
00300		The  object  of  the  new  proof checker will be to present a
00400	system to the user which is usable  for  the  manipulation  of  large
00500	formal  proofs  while at the same time remaining as close to ordinary
00600	mathematical notation and conventions as possible.
00700		Every  attempt will be made to make this portion of the proof
00800	checker independent of specific formal systems.  It will be  presumed
00900	that  the systems in question have axioms and rules of inference, and
01000	that by the action of the rules of inference on  the  axioms  through
01100	the  medium  of  proofs  they  derive  theorems.     Aside from this,
01200	assumptions about the nature of the axioms or the rules of  inference
01300	will be avoided.
01400	
01500		The  first  fundamental  entity  will be called an assertion.
01600	This notion replaces and extends the  usual  notion  of  well  formed
01700	formula  in  most  uses.  Axioms, theorems and lines of proof are the
01800	three most commom examples.  Each assetion contains, in addition to a
01900	well  formed  formula,  a  proper name, a justification, and a set of
02000	assumptions on which it depends.  For example in the case of  a  line
02100	of  proof  these  aspects are clearly visible.  The name is the proof
02200	name together with  the  line  number,  eg.  proof  C  line  17.  The
02300	justification  is  simply  the  command  which produced the line, for
02400	example: modus ponens on lines 2 and  11.   The  set  of  assumptions
02500	contains  the  names  of those assertions on which it depends.  These
02600	will be both the assumption lines in the proof from which it  follows
02700	and axioms from outside the proof on which it relies.